Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
Identifieur interne : 000182 ( Main/Exploration ); précédent : 000181; suivant : 000183Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
Auteurs : Dominique Méry [France] ; Mike Poppleton [Royaume-Uni]Source :
English descriptors
- mix :
Abstract
State-based Formal Methods (e.g Event-B/RODIN \cite{Abr:10,ABH:10}) for critical system development and verification are now well-established, with track records including tool support and industrial applications. The focus of proof-based verification in particular, is on safety properties. Liveness properties, which guarantee {\em eventual}, or converging computations of some requirements, are less well dealt with. Inductive reasoning about liveness is not explicitly supported. Liveness proofs are often complex and expensive, requiring high skill levels on the part of the verification engineer. Fairness-based temporal logic approaches have been proposed to address this, e.g. TLA \cite{lamport94a} and that of Manna \& Pnueli~\cite{DBLP:books/daglib/0080029}. We contribute to this technology need by proposing a fairness-based method integrating temporal and first order logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of Event-B and TLA. Building on our previous work~\cite{MP:13}, we present the method via three example population protocols \cite{AAD:06}. These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network (WSN) and Mobile Ad-Hoc Network (MANET) algorithms. Our examples present typical liveness and convergence requirements. We prove convergence results for the examples by integrated modelling and proof with Event-B/RODIN and TLA. We exploit existing proof rules, define and apply three new proof rules; soundness proofs are also provided. During the process we observe certain repeating patterns in the proofs. These are easily identified and reused because of the explicit nature of the reasoning.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 004E06
- to stream Hal, to step Curation: 004E06
- to stream Hal, to step Checkpoint: 000152
- to stream Main, to step Merge: 000182
- to stream Main, to step Curation: 000182
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems</title><title xml:lang="en" type="sub"> with application to Population Protocols</title><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Poppleton, Mike" sort="Poppleton, Mike" uniqKey="Poppleton M" first="Mike" last="Poppleton">Mike Poppleton</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-394286" status="INCOMING"><orgName>School of Electronics and Computer Science</orgName><desc><address><country key="GB"></country></address></desc><listRelation><relation active="#struct-20409" type="direct"></relation><relation active="#struct-300666" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-20409" type="direct"><org type="laboratory" xml:id="struct-20409" status="VALID"><orgName>School of Electronics and Computer Science</orgName><orgName type="acronym">ECS</orgName><desc><address><addrLine>Electronics and Computer Science University of Southampton SO17 1BJ United Kingdom</addrLine><country key="GB"></country></address><ref type="url">http://www.ecs.soton.ac.uk/</ref></desc><listRelation><relation active="#struct-300666" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300666" type="indirect"><org type="institution" xml:id="struct-300666" status="VALID"><orgName>University of Southampton [Southampton]</orgName><desc><address><addrLine>University RoadSouthampton SO17 1BJ</addrLine><country key="GB"></country></address><ref type="url">http://www.southampton.ac.uk/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Royaume-Uni</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-01245819</idno><idno type="halId">hal-01245819</idno><idno type="halUri">https://hal.inria.fr/hal-01245819</idno><idno type="url">https://hal.inria.fr/hal-01245819</idno><date when="2015-12-17">2015-12-17</date><idno type="wicri:Area/Hal/Corpus">004E06</idno><idno type="wicri:Area/Hal/Curation">004E06</idno><idno type="wicri:Area/Hal/Checkpoint">000152</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000152</idno><idno type="wicri:Area/Main/Merge">000182</idno><idno type="wicri:Area/Main/Curation">000182</idno><idno type="wicri:Area/Main/Exploration">000182</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems</title><title xml:lang="en" type="sub"> with application to Population Protocols</title><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Poppleton, Mike" sort="Poppleton, Mike" uniqKey="Poppleton M" first="Mike" last="Poppleton">Mike Poppleton</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-394286" status="INCOMING"><orgName>School of Electronics and Computer Science</orgName><desc><address><country key="GB"></country></address></desc><listRelation><relation active="#struct-20409" type="direct"></relation><relation active="#struct-300666" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-20409" type="direct"><org type="laboratory" xml:id="struct-20409" status="VALID"><orgName>School of Electronics and Computer Science</orgName><orgName type="acronym">ECS</orgName><desc><address><addrLine>Electronics and Computer Science University of Southampton SO17 1BJ United Kingdom</addrLine><country key="GB"></country></address><ref type="url">http://www.ecs.soton.ac.uk/</ref></desc><listRelation><relation active="#struct-300666" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300666" type="indirect"><org type="institution" xml:id="struct-300666" status="VALID"><orgName>University of Southampton [Southampton]</orgName><desc><address><addrLine>University RoadSouthampton SO17 1BJ</addrLine><country key="GB"></country></address><ref type="url">http://www.southampton.ac.uk/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Royaume-Uni</country></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Correction by Construction</term><term>Event-B method</term><term>Formal Method</term><term>Liveness Properties</term><term>Population Protocols</term><term>Refinement</term><term>TLA+</term><term>Verification & validation</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en"> State-based Formal Methods (e.g Event-B/RODIN \cite{Abr:10,ABH:10}) for critical system development and verification are now well-established, with track records including tool support and industrial applications. The focus of proof-based verification in particular, is on safety properties. Liveness properties, which guarantee {\em eventual}, or converging computations of some requirements, are less well dealt with. Inductive reasoning about liveness is not explicitly supported. Liveness proofs are often complex and expensive, requiring high skill levels on the part of the verification engineer. Fairness-based temporal logic approaches have been proposed to address this, e.g. TLA \cite{lamport94a} and that of Manna \& Pnueli~\cite{DBLP:books/daglib/0080029}. We contribute to this technology need by proposing a fairness-based method integrating temporal and first order logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of Event-B and TLA. Building on our previous work~\cite{MP:13}, we present the method via three example population protocols \cite{AAD:06}. These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network (WSN) and Mobile Ad-Hoc Network (MANET) algorithms. Our examples present typical liveness and convergence requirements. We prove convergence results for the examples by integrated modelling and proof with Event-B/RODIN and TLA. We exploit existing proof rules, define and apply three new proof rules; soundness proofs are also provided. During the process we observe certain repeating patterns in the proofs. These are easily identified and reused because of the explicit nature of the reasoning.</div></front></TEI><affiliations><list><country><li>France</li><li>Royaume-Uni</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Metz</li><li>Nancy</li></settlement><orgName><li>Université de Lorraine</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name></region></country><country name="Royaume-Uni"><noRegion><name sortKey="Poppleton, Mike" sort="Poppleton, Mike" uniqKey="Poppleton M" first="Mike" last="Poppleton">Mike Poppleton</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000182 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000182 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-01245819
|texte= Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems
}}
| This area was generated with Dilib version V0.6.33. |  |